SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

</head>

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

<p><b>ESC/Java</b> (and more recently <b>ESC/Java2</b>), the "Extended Static Checker for Java," is a <a href="../Programming_tool" title="Programming tool">programming tool</a> that attempts to find common <a href="../Run-time_error" class="mw-redirect" title="Run-time error">run-time errors</a> in <a href="../Java_(programming_language)" title="Java (programming language)">Java</a> programs at <a href="../Compile_time" title="Compile time">compile time</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> The underlying approach used in ESC/Java is referred to as <a href="../Extended_static_checking" title="Extended static checking">extended static checking</a>, which is a collective name referring to a range of techniques for <a href="../Static_code_analysis" class="mw-redirect" title="Static code analysis">statically checking</a> the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the <a href="../Bounds_checking" title="Bounds checking">bounds of an array</a>. This technique was pioneered in ESC/Java (and its predecessor, ESC/<a href="../Modula-3" title="Modula-3">Modula-3</a>) and can be thought of as an extended form of <a href="../Type_checking" class="mw-redirect" title="Type checking">type checking</a>. Extended static checking usually involves the use of an <a href="../Automated_theorem_proving" title="Automated theorem proving">automated theorem prover</a> and, in ESC/Java, the Simplify theorem prover was used.

</p><p>ESC/Java is neither <a href="../Soundness" title="Soundness">sound</a> nor <a href="../Completeness_(logic)" title="Completeness (logic)">complete</a>. This was intentional and aims to reduce the number of errors and/or warnings reported to the programmer, in order to make the tool more useful in practice. However, it does mean that: firstly, there are programs that ESC/Java will erroneously consider to be incorrect (known as <i>false-positives</i>); secondly, there are incorrect programs it will consider to be correct (known as <i>false-negatives</i>). Examples in the latter category include errors arising from <a href="../Modular_arithmetic" title="Modular arithmetic">modular arithmetic</a> and/or <a href="../Thread_(computer_science)" class="mw-redirect" title="Thread (computer science)">multithreading</a>.

</p><p>ESC/Java was originally developed at the <a href="../DEC_Systems_Research_Center" title="DEC Systems Research Center">Compaq Systems Research Center</a> (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula-3, ended in 1996. In 2002, SRC released the <a href="../Source_code" title="Source code">source code</a> for ESC/Java and related tools. Recent versions of ESC/Java are based around the <a href="../Java_Modeling_Language" title="Java Modeling Language">Java Modeling Language</a> (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or <i><a href="../Directive_(programming)" title="Directive (programming)">pragmas</a></i>.

</p><p>The <a href="../Radboud_University_Nijmegen" title="Radboud University Nijmegen">University of Nijmegen</a>'s <i>Security of Systems</i> group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the <a href="../Java_Modeling_Language" title="Java Modeling Language">JML</a> specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at <a href="../University_College_Dublin" title="University College Dublin">University College Dublin</a>, which in 2009 moved to the <a href="../IT_University_of_Copenhagen" title="IT University of Copenhagen">IT University of Copenhagen</a>, and in 2012 to the <a href="../Technical_University_of_Denmark" title="Technical University of Denmark">Technical University of Denmark</a>. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple <a href="../Automated_theorem_prover" class="mw-redirect" title="Automated theorem prover">theorem provers</a> and integration with <a href="../Eclipse_(software)" title="Eclipse (software)">Eclipse</a>.

</p><p><a rel="nofollow" class="external text" href="http://www.openjml.org/">OpenJML</a>, the successor of ESC/Java2, is available for Java 1.8.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> The source is available at <a rel="nofollow" class="external free" href="https://github.com/OpenJML">https://github.com/OpenJML</a>

</p><p><sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>

</p>

<ul><li><a href="../Java_Modeling_Language" title="Java Modeling Language">Java Modeling Language</a> (JML)</li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("../mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("../mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("../mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("../mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFFlanaganLeinoLillibridgeNelson2002" class="citation conference cs1">Flanagan, C.; Leino, K.R.M.; Lillibridge, M.; <a href="../Greg_Nelson_(computer_scientist)" title="Greg Nelson (computer scientist)">Nelson, G.</a>; <a href="../James_B._Saxe" title="James B. Saxe">Saxe, J. B.</a>; <a href="../Raymie_Stata" title="Raymie Stata">Stata, R.</a> (2002). <i>Extended static checking for Java</i>. <i>Proceedings of the Conference on Programming Language Design and Implementation</i>. pp. <span class="nowrap">234–</span>245. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F512529.512558">10.1145/512529.512558</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>1-58113-463-0</bdi>.</cite></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://jmlspecs.sourceforge.net/">"OpenJML download site on sourceforge"</a>.</cite></span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJML/">"Java Modeling Language (JML) / Code / [r9606] /OpenJML/Trunk/OpenJML"</a>.</cite></span>

</li>

</ol></div></div>

<dl><dt>Notes</dt></dl>

/* start https://en.wikipedia.org/ */

.mw-parser-output .refbegin{margin-bottom:0.5em}.mw-parser-output .refbegin-hanging-indents>ul{margin-left:0}.mw-parser-output .refbegin-hanging-indents>ul>li{margin-left:0;padding-left:3.2em;text-indent:-3.2em}.mw-parser-output .refbegin-hanging-indents ul,.mw-parser-output .refbegin-hanging-indents ul li{list-style:none}@media(max-width:720px){.mw-parser-output .refbegin-hanging-indents>ul>li{padding-left:1.6em;text-indent:-1.6em}}.mw-parser-output .refbegin-columns{margin-top:0.3em}.mw-parser-output .refbegin-columns ul{margin-top:0}.mw-parser-output .refbegin-columns li{page-break-inside:avoid;break-inside:avoid-column}@media screen{.mw-parser-output .refbegin{font-size:90%}}

/* end https://en.wikipedia.org/ */

</style><div class="refbegin" style="">

<ul><li><cite id="CITEREFFlanaganKiniry2001" class="citation conference cs1">Flanagan, C.; Kiniry, K. R. M. (2001). <i>Houdini, an Annotation Assistant for ESC/Java</i>. <i>FME 2001: Formal Methods for Increasing Software Productivity</i>. Lecture Notes in Computer Science. Vol. 2021. pp. <span class="nowrap">500–</span>517. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F3-540-45251-6_29">10.1007/3-540-45251-6_29</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>3-540-41791-5</bdi>.</cite></li>

<li><cite id="CITEREFCatañoHuisman2002" class="citation conference cs1">Cataño, N.; Huisman, M. (2002). <i>Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java</i>. <i>FME 2002:Formal Methods—Getting IT Right</i>. Lecture Notes in Computer Science. Vol. 2391. pp. <span class="nowrap">272–</span>289. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F3-540-45614-7_16">10.1007/3-540-45614-7_16</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>3-540-43928-5</bdi>.</cite></li>

<li><cite id="CITEREFCokKiniry2005" class="citation conference cs1">Cok, D. R.; Kiniry, J. R. (2005). <i>ESC/Java2: uniting ESC/Java and JML</i>. <i>Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices</i>. Lecture Notes in Computer Science. Vol. 3362. pp. <span class="nowrap">108–</span>128. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-30569-9_6">10.1007/978-3-540-30569-9_6</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>3-540-24287-2</bdi>.</cite></li>

<li><cite id="CITEREFChalinKiniryLeavensPoll2006" class="citation conference cs1">Chalin, P.; Kiniry, J. R.; Leavens, G. T.; Poll, E. (2006). <a rel="nofollow" class="external text" href="https://archive.org/details/formalmethodsfor0000fmco/page/342"><i>Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2</i></a>. <i>Formal Methods for Components and Objects</i>. pp. <a rel="nofollow" class="external text" href="https://archive.org/details/formalmethodsfor0000fmco/page/342">342–363</a>. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F3-540-45614-7_16">10.1007/3-540-45614-7_16</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>3-540-36749-7</bdi>.</cite></li>

<li><cite id="CITEREFCok2006" class="citation conference cs1">Cok, D. R. (2006). <i>Specifying java iterators with JML and Esc/Java2</i>. <i>Proceedings of the 2006 conference on Specification and verification of component-based systems</i>. pp. <span class="nowrap">71–</span>74. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F1181195.1181210">10.1145/1181195.1181210</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>1-59593-586-X</bdi>.</cite></li>

<li><cite id="CITEREFChalin2006" class="citation conference cs1">Chalin, P. (2006). <i>Early detection of JML specification errors using ESC/Java2</i>. <i>Proceedings of the 2006 conference on Specification and verification of component-based systems</i>. pp. <span class="nowrap">25–</span>32. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F1181195.1181201">10.1145/1181195.1181201</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>1-59593-586-X</bdi>.</cite></li>

<li><cite id="CITEREFIshikawa2009" class="citation conference cs1">Ishikawa, H. (2009). <i>An Approach for Refactoring using ESC/Java2: A Simple Case Study</i>. <i>Proceedings of the 2009 conference on New Trends in Software Methodologies, Tools and Techniques</i>. pp. <span class="nowrap">61–</span>72. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-60750-049-0</bdi>.</cite></li>

<li><cite id="CITEREFPoll2009" class="citation conference cs1">Poll, E. (2009). <a rel="nofollow" class="external text" href="https://www.cs.ru.nl/~erikpoll/papers/tfm2009.pdf"><i>Teaching Program Specification and Verification Using JML and ESC/Java2</i></a> <span class="cs1-format">(PDF)</span>. <i>Proceedings of the 2nd International Conference on Teaching Formal Methods</i>. Lecture Notes in Computer Science. Vol. 5846. pp. <span class="nowrap">92–</span>104. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-04912-5_7">10.1007/978-3-642-04912-5_7</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-642-04911-8</bdi>.</cite></li>

<li><cite id="CITEREFJamesChalin2009" class="citation conference cs1">James, P. R.; Chalin, P. (2009). <i>ESC4: a modern caching ESC for Java</i>. <i>Proceedings of the 8th international workshop on Specification and verification of component-based systems</i>. pp. <span class="nowrap">19–</span>26. <a href="../Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F1596486.1596491">10.1145/1596486.1596491</a>. <a href="../ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-60558-680-9</bdi>.</cite></li></ul>

</div>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.hpl.hp.com/downloads/crl/jtk/">Java Programming Toolkit Source Release</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20051208055447/http://research.compaq.com/SRC/esc/">Extended Static Checking for Java</a> at the <a href="../Wayback_Machine" title="Wayback Machine">Wayback Machine</a> (archived December 8, 2005)</li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20051231203805/http://www.kindsoftware.com/products/opensource/ESCJava2/">ESC/Java2 at KindSoftware</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20070208084515/http://gatekeeper.dec.com:80/pub/DEC/SRC/research-reports/abstracts/src-rr-159.html">SRC-RR-159 Extended Static Checking. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20010228175138/http://research.compaq.com/SRC/esc/escm3/download.html">Extended Static Checking Modula-3</a> at the <a href="../Wayback_Machine" title="Wayback Machine">Wayback Machine</a> (archived February 28, 2001)</li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20071002143846/http://www.researchchannel.org/prog/displayevent.aspx?rID=2761">Extended Static Checking</a> Computer Science & Engineering Colloquia. University of Washington. 1999.</li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-19" href="https://en.wikipedia.org/wiki/?title=ESC%2FJava&oldid=1301321423">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>